(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
g(a) → g(b)
b → f(a, a)
f(a, a) → g(d)
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
g(a) → g(b)
b → f(a, a)
f(a, a) → g(d)
Tuples:
G(a) → c(G(b), B)
B → c1(F(a, a))
F(a, a) → c2(G(d))
S tuples:
G(a) → c(G(b), B)
B → c1(F(a, a))
F(a, a) → c2(G(d))
K tuples:none
Defined Rule Symbols:
g, b, f
Defined Pair Symbols:
G, B, F
Compound Symbols:
c, c1, c2
(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)
Removed 2 trailing nodes:
B → c1(F(a, a))
F(a, a) → c2(G(d))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
g(a) → g(b)
b → f(a, a)
f(a, a) → g(d)
Tuples:
G(a) → c(G(b), B)
S tuples:
G(a) → c(G(b), B)
K tuples:none
Defined Rule Symbols:
g, b, f
Defined Pair Symbols:
G
Compound Symbols:
c
(5) CdtRhsSimplificationProcessorProof (BOTH BOUNDS(ID, ID) transformation)
Removed 1 trailing tuple parts
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
g(a) → g(b)
b → f(a, a)
f(a, a) → g(d)
Tuples:
G(a) → c(G(b))
S tuples:
G(a) → c(G(b))
K tuples:none
Defined Rule Symbols:
g, b, f
Defined Pair Symbols:
G
Compound Symbols:
c
(7) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
G(a) → c(G(b))
We considered the (Usable) Rules:
b → f(a, a)
f(a, a) → g(d)
And the Tuples:
G(a) → c(G(b))
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(G(x1)) = [4]x1
POL(a) = [4]
POL(b) = 0
POL(c(x1)) = x1
POL(d) = 0
POL(f(x1, x2)) = 0
POL(g(x1)) = [3]x1
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
g(a) → g(b)
b → f(a, a)
f(a, a) → g(d)
Tuples:
G(a) → c(G(b))
S tuples:none
K tuples:
G(a) → c(G(b))
Defined Rule Symbols:
g, b, f
Defined Pair Symbols:
G
Compound Symbols:
c
(9) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(10) BOUNDS(O(1), O(1))